$\forall$$A$, $C$:Type, $B$:($A$$\rightarrow$Type), $D$:($C$$\rightarrow$Type), ${\it rinv}$:($C$$\rightarrow$($A$+Unit)), $r$:($A$$\rightarrow$$C$), $f$:$c$:$C$ fp$\rightarrow$ $D$($c$).
\\[0ex]inv{-}rel($A$;$C$;$r$;${\it rinv}$) $\Rightarrow$ ($\forall$$a$:$A$. $D$($r$($a$)) $=$ $B$($a$)) $\Rightarrow$ fpf{-}inv{-}rename($r$;${\it rinv}$;$f$) $\in$ $a$:$A$ fp$\rightarrow$ $B$($a$)